Nuprl Lemma : last-reverse
11,40
postcript
pdf
T
:Type,
L
:(
T
List). last(rev(
L
)) ~ hd(
L
)
latex
Definitions
rev(
as
)
,
S
T
,
[
car
/
cdr
]
,
A
List
,
[]
,
Top
,
x
:
A
.
B
(
x
)
,
b
,
Void
,
A
,
P
Q
,
False
,
last(
L
)
,
l
[
i
]
,
i
z
j
,
i
<z
j
,
x
:
A
.
B
(
x
)
,
s
~
t
,
x
:
A
B
(
x
)
,
Type
,
s
=
t
,
type
List
,
t
T
,
hd(
l
)
Lemmas
false
wf
,
not
wf
,
top
wf
,
member
wf
,
reverse
wf
,
last
append
origin
T:Type, L:(T List). last(rev(L)) ~ hd(L) T:Type, L:(T List). last(rev(L)) ~ hd(L) 
T
x:A.B(x)
b
A
Q
z jx:A. B(x)
B(x)
T